The Runtime Complexity (innermost) of the given CpxRelTRS could be proven to be BOUNDS(1, n^1).

0 CpxRelTRS
↳1 RelTrsToTrsProof (UPPER BOUND(ID), 0 ms)
↳2 CpxTRS
    ↳3 CpxTrsMatchBoundsTAProof (⇔, 107 ms)
    ↳4 BOUNDS(1, n^1)
    ↳5 CpxTrsToCdtProof (BOTH BOUNDS(ID, ID), 0 ms)
    ↳6 CdtProblem
        ↳7 CdtLeafRemovalProof (BOTH BOUNDS(ID, ID), 0 ms)
        ↳8 CdtProblem
        ↳9 CdtRhsSimplificationProcessorProof (BOTH BOUNDS(ID, ID), 0 ms)
        ↳10 CdtProblem
        ↳11 CdtUsableRulesProof (⇔, 0 ms)
        ↳12 CdtProblem
        ↳13 CdtRuleRemovalProof (UPPER BOUND(ADD(n^1)), 73 ms)
        ↳14 CdtProblem
        ↳15 CdtRuleRemovalProof (UPPER BOUND(ADD(n^1)), 9 ms)
        ↳16 CdtProblem
        ↳17 SIsEmptyProof (BOTH BOUNDS(ID, ID), 0 ms)
        ↳18 BOUNDS(1, 1)

(0) Obligation:

The Runtime Complexity (innermost) of the given CpxRelTRS could be proven to be BOUNDS(1, n^1).


The TRS R consists of the following rules:

f(C(x1, x2)) → C(f(x1), f(x2))
f(Z) → Z
eqZList(C(x1, x2), C(y1, y2)) → and(eqZList(x1, y1), eqZList(x2, y2))
eqZList(C(x1, x2), Z) → False
eqZList(Z, C(y1, y2)) → False
eqZList(Z, Z) → True
second(C(x1, x2)) → x2
first(C(x1, x2)) → x1
g(x) → x

The (relative) TRS S consists of the following rules:

and(False, False) → False
and(True, False) → False
and(False, True) → False
and(True, True) → True

Rewrite Strategy: INNERMOST

(1) RelTrsToTrsProof (UPPER BOUND(ID) transformation)

transformed relative TRS to TRS

(2) Obligation:

The Runtime Complexity (innermost) of the given CpxTRS could be proven to be BOUNDS(1, n^1).


The TRS R consists of the following rules:

f(C(x1, x2)) → C(f(x1), f(x2))
f(Z) → Z
eqZList(C(x1, x2), C(y1, y2)) → and(eqZList(x1, y1), eqZList(x2, y2))
eqZList(C(x1, x2), Z) → False
eqZList(Z, C(y1, y2)) → False
eqZList(Z, Z) → True
second(C(x1, x2)) → x2
first(C(x1, x2)) → x1
g(x) → x
and(False, False) → False
and(True, False) → False
and(False, True) → False
and(True, True) → True

Rewrite Strategy: INNERMOST

(3) CpxTrsMatchBoundsTAProof (EQUIVALENT transformation)

A linear upper bound on the runtime complexity of the TRS R could be shown with a Match-Bound[TAB_LEFTLINEAR,TAB_NONLEFTLINEAR] (for contructor-based start-terms) of 2.

The compatible tree automaton used to show the Match-Boundedness (for constructor-based start-terms) is represented by:
final states : [1, 2, 3, 4, 5, 6]
transitions:
C0(0, 0) → 0
Z0() → 0
False0() → 0
True0() → 0
f0(0) → 1
eqZList0(0, 0) → 2
second0(0) → 3
first0(0) → 4
g0(0) → 5
and0(0, 0) → 6
f1(0) → 7
f1(0) → 8
C1(7, 8) → 1
Z1() → 1
eqZList1(0, 0) → 9
eqZList1(0, 0) → 10
and1(9, 10) → 2
False1() → 2
True1() → 2
False1() → 6
True1() → 6
C1(7, 8) → 7
C1(7, 8) → 8
Z1() → 7
Z1() → 8
and1(9, 10) → 9
and1(9, 10) → 10
False1() → 9
False1() → 10
True1() → 9
True1() → 10
False2() → 2
False2() → 9
False2() → 10
True2() → 2
True2() → 9
True2() → 10
0 → 3
0 → 4
0 → 5

(4) BOUNDS(1, n^1)

(5) CpxTrsToCdtProof (BOTH BOUNDS(ID, ID) transformation)

Converted Cpx (relative) TRS to CDT

(6) Obligation:

Complexity Dependency Tuples Problem
Rules:

f(C(z0, z1)) → C(f(z0), f(z1))
f(Z) → Z
eqZList(C(z0, z1), C(z2, z3)) → and(eqZList(z0, z2), eqZList(z1, z3))
eqZList(C(z0, z1), Z) → False
eqZList(Z, C(z0, z1)) → False
eqZList(Z, Z) → True
second(C(z0, z1)) → z1
first(C(z0, z1)) → z0
g(z0) → z0
and(False, False) → False
and(True, False) → False
and(False, True) → False
and(True, True) → True
Tuples:

F(C(z0, z1)) → c(F(z0), F(z1))
F(Z) → c1
EQZLIST(C(z0, z1), C(z2, z3)) → c2(AND(eqZList(z0, z2), eqZList(z1, z3)), EQZLIST(z0, z2), EQZLIST(z1, z3))
EQZLIST(C(z0, z1), Z) → c3
EQZLIST(Z, C(z0, z1)) → c4
EQZLIST(Z, Z) → c5
SECOND(C(z0, z1)) → c6
FIRST(C(z0, z1)) → c7
G(z0) → c8
AND(False, False) → c9
AND(True, False) → c10
AND(False, True) → c11
AND(True, True) → c12
S tuples:

F(C(z0, z1)) → c(F(z0), F(z1))
F(Z) → c1
EQZLIST(C(z0, z1), C(z2, z3)) → c2(AND(eqZList(z0, z2), eqZList(z1, z3)), EQZLIST(z0, z2), EQZLIST(z1, z3))
EQZLIST(C(z0, z1), Z) → c3
EQZLIST(Z, C(z0, z1)) → c4
EQZLIST(Z, Z) → c5
SECOND(C(z0, z1)) → c6
FIRST(C(z0, z1)) → c7
G(z0) → c8
AND(False, False) → c9
AND(True, False) → c10
AND(False, True) → c11
AND(True, True) → c12
K tuples:none
Defined Rule Symbols:

f, eqZList, second, first, g, and

Defined Pair Symbols:

F, EQZLIST, SECOND, FIRST, G, AND

Compound Symbols:

c, c1, c2, c3, c4, c5, c6, c7, c8, c9, c10, c11, c12

(7) CdtLeafRemovalProof (BOTH BOUNDS(ID, ID) transformation)

Removed 11 trailing nodes:

G(z0) → c8
AND(True, True) → c12
EQZLIST(Z, Z) → c5
AND(True, False) → c10
AND(False, False) → c9
FIRST(C(z0, z1)) → c7
EQZLIST(Z, C(z0, z1)) → c4
SECOND(C(z0, z1)) → c6
F(Z) → c1
EQZLIST(C(z0, z1), Z) → c3
AND(False, True) → c11

(8) Obligation:

Complexity Dependency Tuples Problem
Rules:

f(C(z0, z1)) → C(f(z0), f(z1))
f(Z) → Z
eqZList(C(z0, z1), C(z2, z3)) → and(eqZList(z0, z2), eqZList(z1, z3))
eqZList(C(z0, z1), Z) → False
eqZList(Z, C(z0, z1)) → False
eqZList(Z, Z) → True
second(C(z0, z1)) → z1
first(C(z0, z1)) → z0
g(z0) → z0
and(False, False) → False
and(True, False) → False
and(False, True) → False
and(True, True) → True
Tuples:

F(C(z0, z1)) → c(F(z0), F(z1))
EQZLIST(C(z0, z1), C(z2, z3)) → c2(AND(eqZList(z0, z2), eqZList(z1, z3)), EQZLIST(z0, z2), EQZLIST(z1, z3))
S tuples:

F(C(z0, z1)) → c(F(z0), F(z1))
EQZLIST(C(z0, z1), C(z2, z3)) → c2(AND(eqZList(z0, z2), eqZList(z1, z3)), EQZLIST(z0, z2), EQZLIST(z1, z3))
K tuples:none
Defined Rule Symbols:

f, eqZList, second, first, g, and

Defined Pair Symbols:

F, EQZLIST

Compound Symbols:

c, c2

(9) CdtRhsSimplificationProcessorProof (BOTH BOUNDS(ID, ID) transformation)

Removed 1 trailing tuple parts

(10) Obligation:

Complexity Dependency Tuples Problem
Rules:

f(C(z0, z1)) → C(f(z0), f(z1))
f(Z) → Z
eqZList(C(z0, z1), C(z2, z3)) → and(eqZList(z0, z2), eqZList(z1, z3))
eqZList(C(z0, z1), Z) → False
eqZList(Z, C(z0, z1)) → False
eqZList(Z, Z) → True
second(C(z0, z1)) → z1
first(C(z0, z1)) → z0
g(z0) → z0
and(False, False) → False
and(True, False) → False
and(False, True) → False
and(True, True) → True
Tuples:

F(C(z0, z1)) → c(F(z0), F(z1))
EQZLIST(C(z0, z1), C(z2, z3)) → c2(EQZLIST(z0, z2), EQZLIST(z1, z3))
S tuples:

F(C(z0, z1)) → c(F(z0), F(z1))
EQZLIST(C(z0, z1), C(z2, z3)) → c2(EQZLIST(z0, z2), EQZLIST(z1, z3))
K tuples:none
Defined Rule Symbols:

f, eqZList, second, first, g, and

Defined Pair Symbols:

F, EQZLIST

Compound Symbols:

c, c2

(11) CdtUsableRulesProof (EQUIVALENT transformation)

The following rules are not usable and were removed:

f(C(z0, z1)) → C(f(z0), f(z1))
f(Z) → Z
eqZList(C(z0, z1), C(z2, z3)) → and(eqZList(z0, z2), eqZList(z1, z3))
eqZList(C(z0, z1), Z) → False
eqZList(Z, C(z0, z1)) → False
eqZList(Z, Z) → True
second(C(z0, z1)) → z1
first(C(z0, z1)) → z0
g(z0) → z0
and(False, False) → False
and(True, False) → False
and(False, True) → False
and(True, True) → True

(12) Obligation:

Complexity Dependency Tuples Problem
Rules:none
Tuples:

F(C(z0, z1)) → c(F(z0), F(z1))
EQZLIST(C(z0, z1), C(z2, z3)) → c2(EQZLIST(z0, z2), EQZLIST(z1, z3))
S tuples:

F(C(z0, z1)) → c(F(z0), F(z1))
EQZLIST(C(z0, z1), C(z2, z3)) → c2(EQZLIST(z0, z2), EQZLIST(z1, z3))
K tuples:none
Defined Rule Symbols:none

Defined Pair Symbols:

F, EQZLIST

Compound Symbols:

c, c2

(13) CdtRuleRemovalProof (UPPER BOUND(ADD(n^1)) transformation)

Found a reduction pair which oriented the following tuples strictly. Hence they can be removed from S.

EQZLIST(C(z0, z1), C(z2, z3)) → c2(EQZLIST(z0, z2), EQZLIST(z1, z3))
We considered the (Usable) Rules:none
And the Tuples:

F(C(z0, z1)) → c(F(z0), F(z1))
EQZLIST(C(z0, z1), C(z2, z3)) → c2(EQZLIST(z0, z2), EQZLIST(z1, z3))
The order we found is given by the following interpretation:
Polynomial interpretation :

POL(C(x1, x2)) = [1] + x1 + x2   
POL(EQZLIST(x1, x2)) = x1   
POL(F(x1)) = 0   
POL(c(x1, x2)) = x1 + x2   
POL(c2(x1, x2)) = x1 + x2   

(14) Obligation:

Complexity Dependency Tuples Problem
Rules:none
Tuples:

F(C(z0, z1)) → c(F(z0), F(z1))
EQZLIST(C(z0, z1), C(z2, z3)) → c2(EQZLIST(z0, z2), EQZLIST(z1, z3))
S tuples:

F(C(z0, z1)) → c(F(z0), F(z1))
K tuples:

EQZLIST(C(z0, z1), C(z2, z3)) → c2(EQZLIST(z0, z2), EQZLIST(z1, z3))
Defined Rule Symbols:none

Defined Pair Symbols:

F, EQZLIST

Compound Symbols:

c, c2

(15) CdtRuleRemovalProof (UPPER BOUND(ADD(n^1)) transformation)

Found a reduction pair which oriented the following tuples strictly. Hence they can be removed from S.

F(C(z0, z1)) → c(F(z0), F(z1))
We considered the (Usable) Rules:none
And the Tuples:

F(C(z0, z1)) → c(F(z0), F(z1))
EQZLIST(C(z0, z1), C(z2, z3)) → c2(EQZLIST(z0, z2), EQZLIST(z1, z3))
The order we found is given by the following interpretation:
Polynomial interpretation :

POL(C(x1, x2)) = [3] + x1 + x2   
POL(EQZLIST(x1, x2)) = [3] + [2]x1 + [2]x2   
POL(F(x1)) = [3] + [3]x1   
POL(c(x1, x2)) = x1 + x2   
POL(c2(x1, x2)) = x1 + x2   

(16) Obligation:

Complexity Dependency Tuples Problem
Rules:none
Tuples:

F(C(z0, z1)) → c(F(z0), F(z1))
EQZLIST(C(z0, z1), C(z2, z3)) → c2(EQZLIST(z0, z2), EQZLIST(z1, z3))
S tuples:none
K tuples:

EQZLIST(C(z0, z1), C(z2, z3)) → c2(EQZLIST(z0, z2), EQZLIST(z1, z3))
F(C(z0, z1)) → c(F(z0), F(z1))
Defined Rule Symbols:none

Defined Pair Symbols:

F, EQZLIST

Compound Symbols:

c, c2

(17) SIsEmptyProof (BOTH BOUNDS(ID, ID) transformation)

The set S is empty

(18) BOUNDS(1, 1)